P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
Q1(p(q(x1))) → Q2(p(Q(x1)))
Q2(q(p(x1))) → Q2(x1)
P1(x1) → P2(x1)
Q1(p(q(x1))) → P2(Q(x1))
P1(x1) → Q1(Q(p(x1)))
P2(p(x1)) → Q2(x1)
Q2(q(p(x1))) → P2(q(q(x1)))
P2(Q(Q(x1))) → Q1(p(x1))
P2(Q(Q(x1))) → Q1(Q(p(x1)))
P2(Q(Q(x1))) → P2(x1)
P2(p(x1)) → Q2(q(x1))
Q1(p(q(x1))) → Q1(x1)
P1(x1) → Q1(p(x1))
Q2(q(p(x1))) → Q2(q(x1))
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q1(p(q(x1))) → Q2(p(Q(x1)))
Q2(q(p(x1))) → Q2(x1)
P1(x1) → P2(x1)
Q1(p(q(x1))) → P2(Q(x1))
P1(x1) → Q1(Q(p(x1)))
P2(p(x1)) → Q2(x1)
Q2(q(p(x1))) → P2(q(q(x1)))
P2(Q(Q(x1))) → Q1(p(x1))
P2(Q(Q(x1))) → Q1(Q(p(x1)))
P2(Q(Q(x1))) → P2(x1)
P2(p(x1)) → Q2(q(x1))
Q1(p(q(x1))) → Q1(x1)
P1(x1) → Q1(p(x1))
Q2(q(p(x1))) → Q2(q(x1))
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
Q2(q(p(x1))) → P2(q(q(x1)))
P2(Q(Q(x1))) → Q1(p(x1))
P2(Q(Q(x1))) → Q1(Q(p(x1)))
P2(Q(Q(x1))) → P2(x1)
Q1(p(q(x1))) → Q2(p(Q(x1)))
Q1(p(q(x1))) → Q1(x1)
Q2(q(p(x1))) → Q2(x1)
P2(p(x1)) → Q2(q(x1))
Q2(q(p(x1))) → Q2(q(x1))
Q1(p(q(x1))) → P2(Q(x1))
P2(p(x1)) → Q2(x1)
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P2(Q(Q(x1))) → Q1(p(x1))
P2(Q(Q(x1))) → P2(x1)
Q1(p(q(x1))) → Q1(x1)
Q2(q(p(x1))) → Q2(x1)
Q2(q(p(x1))) → Q2(q(x1))
Q1(p(q(x1))) → P2(Q(x1))
P2(p(x1)) → Q2(x1)
Used ordering: Polynomial interpretation [25,35]:
Q2(q(p(x1))) → P2(q(q(x1)))
P2(Q(Q(x1))) → Q1(Q(p(x1)))
Q1(p(q(x1))) → Q2(p(Q(x1)))
P2(p(x1)) → Q2(q(x1))
The value of delta used in the strict ordering is 16.
POL(Q2(x1)) = (4)x_1
POL(Q(x1)) = 4 + x_1
POL(P(x1)) = (2)x_1
POL(q(x1)) = 4 + x_1
POL(p(x1)) = 4 + x_1
POL(P2(x1)) = (4)x_1
POL(Q1(x1)) = (4)x_1
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
p(p(x1)) → q(q(x1))
q(q(p(x1))) → p(q(q(x1)))
Q(q(x1)) → x1
q(Q(x1)) → x1
p(P(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
Q2(q(p(x1))) → P2(q(q(x1)))
P2(Q(Q(x1))) → Q1(Q(p(x1)))
Q1(p(q(x1))) → Q2(p(Q(x1)))
P2(p(x1)) → Q2(q(x1))
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P2(Q(Q(x1))) → Q1(Q(p(x1)))
Q1(p(q(x1))) → Q2(p(Q(x1)))
Used ordering: Polynomial interpretation [25,35]:
Q2(q(p(x1))) → P2(q(q(x1)))
P2(p(x1)) → Q2(q(x1))
The value of delta used in the strict ordering is 1/8.
POL(Q2(x1)) = (1/4)x_1
POL(Q(x1)) = 1/4 + (4)x_1
POL(P(x1)) = (4)x_1
POL(q(x1)) = (1/2)x_1
POL(p(x1)) = (2)x_1
POL(P2(x1)) = x_1
POL(Q1(x1)) = 1/4 + (2)x_1
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
p(p(x1)) → q(q(x1))
q(q(p(x1))) → p(q(q(x1)))
Q(q(x1)) → x1
q(Q(x1)) → x1
p(P(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
Q2(q(p(x1))) → P2(q(q(x1)))
P2(p(x1)) → Q2(q(x1))
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
Q2(q(p(x1))) → P2(q(q(x1)))
P2(p(x1)) → Q2(q(x1))
The value of delta used in the strict ordering is 1.
POL(Q2(x1)) = (4)x_1
POL(Q(x1)) = x_1
POL(P(x1)) = 1 + (4)x_1
POL(q(x1)) = x_1
POL(p(x1)) = 1/4 + x_1
POL(P2(x1)) = (4)x_1
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
p(p(x1)) → q(q(x1))
q(q(p(x1))) → p(q(q(x1)))
Q(q(x1)) → x1
q(Q(x1)) → x1
p(P(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1